A, B:Realizer. A || B  (i:Id. R-da(A;i) || R-da(B;i)) 

latex

Definitions

, t  T, {x:A| B(x) }, x:AB(x), #$n, a<b, Void, False, A, , ij, -n, n-m, R-size(R), n+m, R-da(R;i), KindDeq, Type, Knd, f || g, Id, x:A. B(x), A || B, P  Q, AB, Realizer, , es realizer ind Rplus compseq tag def, b, b, , s = t, Prop, Rplus?(x1), x:AB(x), P & Q, P  Q, {T}, SQType(T), s ~ t, left+right, P  Q, Rplus-right(x1), Rplus-left(x1), x.A(x), x. t(x), f  g, es realizer ind Rnone compseq tag def, Rnone?(x1), Top, a:A fp B(a), x:A. B(x), Rda(R), R-loc(R), a = b, Unit, , if b t else f fi, Atom$n, True, P  Q, T, EqDecider(T), f(a), x(s)

Lemmas

fpf-compatible wf, squash wf, true wf, deq wf, R-da-Rda, Id sq, ifthenelse wf, fpf-empty wf, not functionality wrt iff, assert-eq-id, eq id wf, R-loc wf, Rda wf, fpf-empty-compatible-right, fpf-empty-compatible-left, fpf-trivial-subtype-top, fpf wf, top wf, Rnone? wf, Rnone-implies, R-size-decreases, fpf-compatible-symmetry, fpf-join wf, fpf-compatible-join, Kind-deq wf, Knd wf, R-da wf, R-compat-symmetry, Rplus-left wf, Rplus-right wf, bool cases, eqtt to assert, bool sq, iff transitivity, eqff to assert, assert of bnot, Rplus? wf, bool wf, bnot wf, not wf, assert wf, Rplus-implies, ge wf, nat properties, nat wf, Id wf, R-compat wf, es realizer wf, le wf, R-size wf, nat plus wf